-- ========================================================================
--         predicate conjunctions through predicate names 
-- ========================================================================

-- ========================================================================
-- defining the conjunction of predicates
-- via the sequence of the names of the predicates
mod! PREDcj (X :: TRIV) {
-- names of predicates on Elt.X and the sequences of the names
[Pname < PnameSeq]
** an element of Pname is an element of PnameSeq
-- associative binary operator for constructing 
-- non nil sequences
op _ _ : PnameSeq PnameSeq -> PnameSeq {constr assoc}
** (pn_1 pn_2 ... pn_k) is of the sort PnameSeq
** if pn_1, pn_2, ..., pn_k are of the sort Pname
-- cj(pns,e) defines the conjunction of predicates 
-- whose names constitute the sequence pns
op cj : PnameSeq Elt -> Bool .
eq cj((PN:Pname PNS:PnameSeq),E:Elt) = cj(PN,E) and cj(PNS,E) .
** cj((pn_1 pn_2 ... pn_k),e)
**   = cj(pn_1,e) and cj(pn_2,e) and ... and cj(pn_k,e) .
}

-- ========================================================================
provide predCj

-- ========================================================================
eof